DECLARE PREDPAR Q(NATNUM,NATNUM);
∧I INDUCTION[P←λN.
(Q(0,N)⊃∃N1 K.(Q(K,N1)∧(N1=0∧K=M*N ∨ ¬(N1=0)∧¬Q(K+M,PRED N1))))];
ASSUME Q(0,0);
ASSUME ∀N1 K.¬(Q(K,N1)∧(N1=0∧K=M*0∨¬(N1=0)∧¬Q(K+M,PRED N1)));
∀E 3 0 0;
∀E TIMES1 M;
TAUTEQ FALSE 2:5;
¬I 6 3;
UNIFY ∃N1 K.7:#1#1#1 7;
TAUTEQ 7:#1#1#1 = 7:#1#1#1;
UNIFY ∃N1 K.(Q(K,N1)∧((N1=0∧K=(M*0))∨(¬(N1=0)∧¬Q(K+M,PRED N1)))) 7;
UNIFY  ∃N1 K.7:#1#1#1#1 ,7;
⊃I 2 8;
ASSUME 1:#1#2#1#1;
ASSUME Q(0,SUCC N);